perm filename DEMO.PR1[258,JMC] blob
sn#146360 filedate 1975-02-18 generic text, type T, neo UTF8
1 (((M+N)+0)=(M+(N+0))∧∀N1.(((M+N)+N1)=(M+(N+N1))⊃((M+N)+SUCC N1)=(M+(N+SUCC N1))))⊃∀N1.((M+N)+N1)=(M+(N+N1)) %
∧I (INDUCTION)
2 ((M+N)+0)=(M+N) ∀E PLUS1 M+N
3 (N+0)=N ∀E PLUS1 N
4 (M+N)=(M+N) TAUTEQ
5 (M+(N+0))=(M+N) SUBST 3 IN 4 OCC (1)
6 ∀N1.(((M+N)+N1)=(M+(N+N1))⊃((M+N)+SUCC N1)=(M+(N+SUCC N1)))⊃∀N1.((M+N)+N1)=(M+(N+N1)) TAUTEQ
7 ((M+N)+N1)=(M+(N+N1)) (7) ASSUME
8 ((M+N)+SUCC N1)=SUCC ((M+N)+N1) ∀E PLUS2 M+N , N1
9 ((M+N)+SUCC N1)=SUCC (M+(N+N1)) (7) SUBSTR 7 IN 8
10 (M+SUCC (N+N1))=SUCC (M+(N+N1)) ∀E PLUS2 M , N+N1
11 (N+SUCC N1)=SUCC (N+N1) ∀E PLUS2 N , N1
12 (M+(N+SUCC N1))=SUCC (M+(N+N1)) SUBST 11 IN 10
13 ((M+N)+SUCC N1)=(M+(N+SUCC N1)) (7) TAUTEQ
14 ((M+N)+N1)=(M+(N+N1))⊃((M+N)+SUCC N1)=(M+(N+SUCC N1)) ⊃I 7 13
15 ∀N1.(((M+N)+N1)=(M+(N+N1))⊃((M+N)+SUCC N1)=(M+(N+SUCC N1))) ∀I 14 N1 ← N1
16 ∀N1.((M+N)+N1)=(M+(N+N1)) ⊃E 15 6
17 ((M+N)+K)=(M+(N+K)) ∀E 16 K
18 ∀M N K.((M+N)+K)=(M+(N+K)) ∀I 17 M ← M N ← N K ← K
19 ((0+0)=0∧∀N.((0+N)=N⊃(0+SUCC N)=SUCC N))⊃∀N.(0+N)=N ∧I (INDUCTION)
20 (0+0)=0 ∀E PLUS1 0
21 ∀N.((0+N)=N⊃(0+SUCC N)=SUCC N)⊃∀N.(0+N)=N TAUT
22 (0+N)=N (22) ASSUME
23 (0+SUCC N)=SUCC (0+N) ∀E PLUS2 0 , N
24 (0+SUCC N)=SUCC N (22) SUBSTR 22 IN 23
25 (0+N)=N⊃(0+SUCC N)=SUCC N ⊃I 22 24
26 ∀N.((0+N)=N⊃(0+SUCC N)=SUCC N) ∀I 25 N ← N
27 ∀N.(0+N)=N ⊃E 26 21
28 ((0+1)=SUCC 0∧∀N.((N+1)=SUCC N⊃(SUCC N+1)=SUCC SUCC N))⊃∀N.(N+1)=SUCC N ∧I (INDUCTION)
29 (0+1)=1 ∀E 27 1
30 ∀N.((N+1)=SUCC N⊃(SUCC N+1)=SUCC SUCC N)⊃∀N.(N+1)=SUCC N TAUTEQ
31 (N+1)=SUCC N (31) ASSUME
32 (SUCC N+1)=(SUCC N+1) TAUTEQ
33 (SUCC N+1)=(SUCC N+SUCC 0) SUBSTR ONE IN 32 OCC (2)
34 (SUCC N+SUCC 0)=SUCC (SUCC N+0) ∀E PLUS2 SUCC N , 0
35 (SUCC N+0)=SUCC N ∀E PLUS1 SUCC N
36 (SUCC N+SUCC 0)=SUCC SUCC N SUBSTR 35 IN 34
37 (SUCC N+1)=SUCC SUCC N TAUTEQ
38 (N+1)=SUCC N⊃(SUCC N+1)=SUCC SUCC N ⊃I 31 37
39 ∀N.((N+1)=SUCC N⊃(SUCC N+1)=SUCC SUCC N) ∀I 38 N ← N
40 ∀N.(N+1)=SUCC N ⊃E 39 30
41 ((1+0)=SUCC 0∧∀N.((1+N)=SUCC N⊃(1+SUCC N)=SUCC SUCC N))⊃∀N.(1+N)=SUCC N ∧I (INDUCTION)
42 (1+0)=1 ∀E PLUS1 1
43 ∀N.((1+N)=SUCC N⊃(1+SUCC N)=SUCC SUCC N)⊃∀N.(1+N)=SUCC N TAUTEQ
44 (1+N)=SUCC N (44) ASSUME
45 (1+SUCC N)=SUCC (1+N) ∀E PLUS2 1 , N
46 (1+SUCC N)=SUCC SUCC N (44) SUBSTR 44 IN 45
47 (1+N)=SUCC N⊃(1+SUCC N)=SUCC SUCC N ⊃I 44 46
48 ∀N.((1+N)=SUCC N⊃(1+SUCC N)=SUCC SUCC N) ∀I 47 N ← N
49 ∀N.(1+N)=SUCC N ⊃E 48 43
50 (∀M.((M+0)-0)=M∧∀N.(∀M.((M+N)-N)=M⊃∀M.((M+SUCC N)-SUCC N)=M))⊃∀N M.((M+N)-N)=M ∧I (INDUCTION)
51 (M+0)=M ∀E PLUS1 M
52 ((M+0)-0)=(M+0) ∀E MINUS2 M+0
53 ((M+0)-0)=M TAUTEQ
54 ∀M.((M+0)-0)=M ∀I 53 M ← M
55 ∀N.(∀M.((M+N)-N)=M⊃∀M.((M+SUCC N)-SUCC N)=M)⊃∀N M.((M+N)-N)=M TAUT
56 ∀M.((M+N)-N)=M (56) ASSUME
57 ((M+SUCC N)-SUCC N)=PRED ((M+SUCC N)-N) ∀E MINUS3 M+SUCC N , N
58 (1+N)=SUCC N ∀E 49 N
59 ((M+SUCC N)-SUCC N)=PRED ((M+(1+N))-N) SUBST 58 IN 57 OCC (3)
60 ((M+1)+N)=(M+(1+N)) ∀E 18 M , 1 , N
61 ((M+SUCC N)-SUCC N)=PRED (((M+1)+N)-N) SUBST 60 IN 59
62 (M+1)=SUCC M ∀E 40 M
63 ((M+SUCC N)-SUCC N)=PRED ((SUCC M+N)-N) SUBSTR 62 IN 61
64 ((SUCC M+N)-N)=SUCC M (56) ∀E 56 SUCC M
65 ((M+SUCC N)-SUCC N)=PRED SUCC M (56) SUBSTR 64 IN 63
66 PRED SUCC M=M ∀E PEANO2 M
67 ((M+SUCC N)-SUCC N)=M (56) SUBSTR 66 IN 65
68 ∀M.((M+SUCC N)-SUCC N)=M (56) ∀I 67 M ← M
69 ∀M.((M+N)-N)=M⊃∀M.((M+SUCC N)-SUCC N)=M ⊃I 56 68
70 ∀N.(∀M.((M+N)-N)=M⊃∀M.((M+SUCC N)-SUCC N)=M) ∀I 69 N ← N
71 ∀N M.((M+N)-N)=M ⊃E 55 70
72 ((0+N)-N)=0 ∀E 71 N , 0
73 (0+N)=N ∀E 27 N
74 (N-N)=0 SUBSTR 73 IN 72
75 ∀N.(N-N)=0 ∀I 74 N ← N